perm filename IMPURE.XGP[F77,JMC] blob sn#316829 filedate 1977-11-11 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=NGR25/FONT#6=NGR20/FONT#7=MATH30/FONT#9=GRK30/FONT#10=MS25/FONT#11=GRFX25/FONT#12=GRFX35
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓α␈↓ ¬{Chapter IV

␈↓ ↓H␈↓α␈↓ βVIMPURE PROGRAMS AND UNCLEAN PROGRAMS


␈↓ ↓H␈↓        Pure␈α
clean␈α∞LISP␈α
programs␈α∞admit␈α
the␈α
elegant␈α∞mathematical␈α
characterization␈α∞described␈α
and
␈↓ ↓H␈↓applied␈α⊂in␈α⊂Chapter␈α∂3.␈α⊂ Specifically,␈α⊂each␈α∂recursively␈α⊂defined␈α⊂pure␈α∂clean␈α⊂LISP␈α⊂function␈α⊂can␈α∂be
␈↓ ↓H␈↓translated␈αinto␈αa␈αfunctional␈αequation␈αand␈αminimization␈αschema␈αin␈αa␈αfirst␈αorder␈αlanguage,␈αand␈αthe
␈↓ ↓H␈↓function and schema can be used to prove that the program meets its extensional specifications.

␈↓ ↓H␈↓        In␈α⊂this␈α∂chapter␈α⊂we␈α∂shall␈α⊂describe␈α∂some␈α⊂additional␈α∂features␈α⊂of␈α∂practical␈α⊂LISP␈α⊂systems␈α∂for
␈↓ ↓H␈↓which␈α
good␈α
simple␈α
mathematical␈α
characterizations␈α
have␈α
not␈α
yet␈α
been␈α
found.␈α
 Every␈α
computation
␈↓ ↓H␈↓that␈αcan␈αbe␈αdone␈α
with␈αthese␈αfeatures␈αcan␈α
be␈αdone␈αin␈αpure␈α
clean␈αLISP,␈αbut␈αnevertheless␈α
there␈αare
␈↓ ↓H␈↓often␈α
good␈α
reasons␈α
for␈α
using␈α
these␈α
features.␈α
 We␈α
shall␈α
examine␈α
the␈α
features␈α
themselves␈α∞and␈α
also
␈↓ ↓H␈↓the criteria that determine when they should be used in preference to pure clean LISP.

␈↓ ↓H␈↓        All␈α⊗these␈α⊗features␈α⊗can␈α⊗be␈α∃formalized␈α⊗in␈α⊗terms␈α⊗of␈α⊗their␈α∃effect␈α⊗on␈α⊗the␈α⊗"state␈α⊗of␈α∃the
␈↓ ↓H␈↓computation",␈αand␈αthis␈αhas␈αbeen␈αdone␈αby␈αMichael␈αGordon␈α(197x),␈αbut␈αhis␈αformalizations␈αseem␈αtoo
␈↓ ↓H␈↓complicated␈αfor␈αelementary␈αexposition.␈α The␈αgeneral␈αidea␈αis␈αto␈αintroduce␈αa␈αstate␈αvariable␈α␈↓	x␈↓␈αand␈αto
␈↓ ↓H␈↓describe the "execution" of expressions as functions on states that produce new states.



␈↓ ↓H␈↓1.  ␈↓αSequential (Algol-like) programs.␈↓


␈↓ ↓H␈↓        Sequential␈α∪programs␈α∪are␈α∀impure␈α∪(by␈α∪definition),␈α∪but␈α∀can␈α∪be␈α∪clean␈α∪-␈α∀provided␈α∪certain
␈↓ ↓H␈↓restrictions␈αare␈αobserved.␈α The␈αexternal␈αnotation␈αfor␈αsequential␈αprograms␈αis␈αadapted␈αfrom␈αthat␈αof
␈↓ ↓H␈↓Algol 60.  We allow as a term an expression of the form

␈↓ ↓H␈↓        ␈↓↓program[<variable list>,<statement list>]␈↓,

␈↓ ↓H␈↓where␈α␈↓↓<variable␈α
list>␈↓␈αis␈α
a␈αlist␈αof␈α
variables␈αlocal␈α
to␈αthe␈α
program,␈αand␈α␈↓↓<statement␈α
list>␈↓␈αis␈α
a␈αlist␈αof␈α
the
␈↓ ↓H␈↓statements␈α
of␈α
the␈αprogram.␈α
 As␈α
in␈αAlgol␈α
60,␈α
the␈αstatements␈α
are␈α
separated␈αby␈α
semicolons,␈α
and␈αany
␈↓ ↓H␈↓statement may be preceded by a label followed by a colon.

␈↓ ↓H␈↓        The statements are of the following kinds:

␈↓ ↓H␈↓        1. Assignment statements of the form

␈↓ ↓H␈↓        ␈↓↓<left hand side> ← <right hand side>␈↓,

␈↓ ↓H␈↓where␈α⊃␈↓↓<left␈α⊃hand␈α⊃side>␈↓␈α⊃is␈α⊃a␈α⊃variable,␈α⊃possibly␈α⊃subscripted,␈α⊃and␈α⊃␈↓↓<right␈α⊃hand␈α⊃side>␈↓␈α⊃is␈α⊃a␈α⊃LISP
␈↓ ↓H␈↓expression that can be evaluated.

␈↓ ↓H␈↓        2. ␈↓αgo to␈↓ statements of the form

␈↓ ↓H␈↓        ␈↓αgo to␈↓↓ a␈↓
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 92


␈↓ ↓H␈↓where␈α
␈↓↓a␈↓␈α
is␈α
a␈α
label␈α
or␈α
an␈α
expression␈α
that␈α
evaluates␈α
to␈α
a␈α
label.␈α
 Since␈α
labels␈α
are␈α
atoms␈α
in␈αinternal
␈↓ ↓H␈↓notation,␈α
any␈α
expression␈α
evaluating␈α
to␈α
an␈α
atom␈α
may␈αbe␈α
used,␈α
but␈α
the␈α
usual␈α
case␈α
is␈α
a␈αconditional
␈↓ ↓H␈↓expression␈αwherein␈α
the␈αsecond␈α
element␈αof␈α
each␈αpair␈αis␈α
an␈αatom.␈α
 Should␈αthe␈α
resulting␈αexpression
␈↓ ↓H␈↓not be an atom or should that atom not be used as a label, an error message will be generated.

␈↓ ↓H␈↓        3. A conditional statement which has the form

␈↓ ↓H␈↓        ␈↓↓␈↓αif␈↓↓ p1 ␈↓αthen␈↓↓ s1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ... ␈↓αelse␈↓↓ ␈↓αif␈↓↓ pn ␈↓αelse␈↓↓ sn␈↓,

␈↓ ↓H␈↓where the ␈↓↓p␈↓'s are propositional expressions having truth values, and the ␈↓↓s␈↓'s are any statements.

␈↓ ↓H␈↓        4. ␈↓αreturn␈↓↓ e␈↓

␈↓ ↓H␈↓where␈α␈↓↓e␈↓␈αis␈αan␈αarbitrary␈αexpression.␈α The␈α
effect␈αof␈αexecuting␈αthis␈αexpression␈αis␈αto␈αreturn␈α
from␈αthe
␈↓ ↓H␈↓program giving the program as a term the value of the expression ␈↓↓e␈↓.

␈↓ ↓H␈↓        As an example, we might write ␈↓↓reverse␈↓ as follows:

␈↓ ↓H␈↓        ␈↓↓reverse u ← ␈↓αprogram␈↓↓[[v];
␈↓ ↓H␈↓↓                v ← ␈↓¬NIL␈↓↓;
␈↓ ↓H␈↓↓        a:      ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ ␈↓αreturn␈↓↓ v;
␈↓ ↓H␈↓↓                v ← ␈↓αa␈↓↓␈α∧u . v;
␈↓ ↓H␈↓↓                u ← ␈↓αd␈↓↓␈α∧v;
␈↓ ↓H␈↓↓                ␈↓αgo to␈↓ a].

␈↓ ↓H␈↓        The internal form of the same program is

␈↓ ↓H␈↓        (DE REVERSE (U) (PROG (V)
␈↓ ↓H␈↓                (SETQ V NIL)
␈↓ ↓H␈↓                A
␈↓ ↓H␈↓                (COND ((NULL U) (RETURN V)))
␈↓ ↓H␈↓                (SETQ V (CONS (CAR U) V))
␈↓ ↓H␈↓                (SETQ U (CDR U))
␈↓ ↓H␈↓                (GO A)
␈↓ ↓H␈↓        ))

␈↓ ↓H␈↓where␈αthe␈αparagraphing␈αis␈αonly␈αfor␈αthe␈αreader's␈αconvenience.␈α Notice␈αthat␈αin␈αinternal␈αform,␈αlabels
␈↓ ↓H␈↓are statements rather than attachments to statements.

␈↓ ↓H␈↓        Here are some ways we might write ␈↓↓append␈↓:

␈↓ ↓H␈↓        ␈↓↓u * v ← ␈↓αprogram␈↓↓[
␈↓ ↓H␈↓↓                ␈↓αreturn␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓␈α∧u . [␈↓αd␈↓↓␈α∧u * v]]␈↓,


␈↓ ↓H␈↓is just a trivial rewrite of the recursive definition.

␈↓ ↓H␈↓        ␈↓↓u * v ← ␈↓αprog␈↓↓ram[w;
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 93


␈↓ ↓H␈↓↓                ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ ␈↓αreturn␈↓↓ v;
␈↓ ↓H␈↓↓                w ← ␈↓αa␈↓↓␈α∧u . [␈↓αd␈↓↓␈α∧u * v];
␈↓ ↓H␈↓↓                ␈↓αreturn␈↓↓ w]␈↓


␈↓ ↓H␈↓is␈αalmost␈α
as␈αclose␈α
to␈αthe␈α
pure␈αLISP␈α
form.␈α If␈αwe␈α
want␈αto␈α
replace␈αthe␈α
recursion␈αby␈α
a␈αloop,␈α
we␈αcan
␈↓ ↓H␈↓write
␈↓ ↓H␈↓        ␈↓↓u * v ← ␈↓αprog␈↓↓ram[w, u1, v1;
␈↓ ↓H␈↓↓                w ← ␈↓¬NIL␈↓↓;
␈↓ ↓H␈↓↓                u1 ← u;
␈↓ ↓H␈↓↓                v1 ← v;
␈↓ ↓H␈↓↓        a:      ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u1 ␈↓αthen␈↓↓ ␈↓αgo to* b;
␈↓ ↓H␈↓α                w ← a␈α∧u1 . w;
␈↓ ↓H␈↓α                u1 ← d␈α∧u;
␈↓ ↓H␈↓α                go to* a;
␈↓ ↓H␈↓α        b:      if n␈α∧w then return v1;
␈↓ ↓H␈↓α                v1 ← a␈α∧w . v1;
␈↓ ↓H␈↓α                ␈↓πT␈↓α ← d␈α∧w;
␈↓ ↓H␈↓α                go to* b]␈↓.


␈↓ ↓H␈↓This corresponds to the recursive program

␈↓ ↓H␈↓        ␈↓↓u * v ← app[u,v,␈↓¬NIL␈↓↓]

␈↓ ↓H␈↓↓        app[u,v,w] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ [␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧w ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ app[u,␈↓αa␈↓↓␈α∧w . v,␈↓αd␈↓↓␈α∧w]]
␈↓ ↓H␈↓↓␈↓αelse␈↓↓ app[␈↓αd␈↓↓␈α∧u,v,␈↓αa␈↓↓␈α∧u . w]␈↓


␈↓ ↓H␈↓which can save some storage if it is compiled or interpreted without using the stack.

␈↓ ↓H␈↓        We␈αshall␈α
not␈αtreat␈αthe␈α
mathematics␈αof␈αsequential␈α
programs␈αfully␈αat␈α
this␈αpoint.␈α
 However,␈αa
␈↓ ↓H␈↓sequential␈α∂program␈α∞that␈α∂occurs␈α∂as␈α∞a␈α∂term␈α∞can␈α∂be␈α∂replaced␈α∞by␈α∂a␈α∞term␈α∂involving␈α∂only␈α∞functional
␈↓ ↓H␈↓programs provided the following conditions are observed:

␈↓ ↓H␈↓        1.␈αAll␈α
variables␈αlocal␈α
to␈αthe␈αprogram␈α
are␈αinitialized␈α
before␈αbeing␈αused.␈α
 Of␈αcourse,␈α
it␈αcould
␈↓ ↓H␈↓be␈αtaken␈α
as␈αa␈αconvention␈α
that␈αthese␈α
variables␈αare␈αinitialized␈α
to␈α␈↓¬NIL␈↓␈αwhen␈α
the␈αprogram␈α
is␈αentered.
␈↓ ↓H␈↓Then␈αit␈αwouldn't␈αaffect␈αthe␈αcorrectness␈αof␈αthe␈αtranslation␈αto␈αa␈αfunctional␈αprogram␈αif␈αsome␈αof␈αthem
␈↓ ↓H␈↓weren't further initialized.

␈↓ ↓H␈↓        2. All assignments are to variables local to the program.

␈↓ ↓H␈↓        A␈α
new␈αfunction␈α
definition␈α
is␈αmade␈α
for␈α
each␈αbranch␈α
(i.e.␈α
 conditional␈α␈↓αgo to␈↓)␈α
in␈α
the␈αoriginal
␈↓ ↓H␈↓program.␈α The␈αargument␈α
of␈αthe␈αfunction␈αis␈α
a␈αlist␈αwhose␈αelements␈α
are␈αvalues␈αassigned␈αto␈α
the␈αlocal
␈↓ ↓H␈↓variables,␈αi.e.␈α
the␈αlist␈α
has␈αas␈α
many␈αelements␈α
as␈αthere␈α
are␈αlocal␈α
variables.␈α The␈α
value␈αof␈αthe␈α
function
␈↓ ↓H␈↓is␈α
the␈αvalue␈α
that␈αwill␈α
be␈α
␈↓αreturn␈↓ed␈αfrom␈α
the␈αprogram␈α
given␈α
that␈αthe␈α
local␈αvariables␈α
have␈αthe␈α
values
␈↓ ↓H␈↓given␈αin␈αthe␈α
argument␈αwhen␈αthe␈αbranch␈α
is␈αreached.␈α The␈α␈↓αprogram␈↓␈α
expression␈αitself␈αis␈αreplaced␈α
by
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 94


␈↓ ↓H␈↓an␈α
application␈α∞of␈α
the␈α∞function␈α
corresponding␈α∞to␈α
the␈α
first␈α∞branch␈α
encountered␈α∞in␈α
the␈α∞program␈α
to
␈↓ ↓H␈↓the␈α∂state␈α∞vector␈α∂whose␈α∞components␈α∂have␈α∞the␈α∂values␈α∞they␈α∂will␈α∞have␈α∂the␈α∞first␈α∂time␈α∞the␈α∂branch␈α∞is
␈↓ ↓H␈↓reached written as functions of the external variables.

␈↓ ↓H␈↓        As␈αan␈αexample,␈αconsider␈αthe␈αfollowing␈αexpression␈αthat␈αgives␈αthe␈αresult␈αof␈αappending␈αthe␈αlist
␈↓ ↓H␈↓␈↓↓a␈↓ with the reversal of ␈↓↓a*b␈↓:

␈↓ ↓H␈↓        ␈↓↓a␈α*␈α␈↓αprogram␈↓↓[[u,v]␈αu␈α←␈αa␈α*␈αb;␈αv␈α←␈α␈↓¬NIL␈↓↓;␈αloop:␈α␈↓αif␈↓↓␈α␈↓αn␈↓↓␈α∧u␈α␈↓αthen␈↓↓␈α␈↓αreturn␈↓↓␈αv;␈αv␈α←␈α␈↓αa␈↓↓␈α∧u␈α.␈αv;␈αu␈α←␈α␈↓αd␈↓↓␈α∧u;␈α␈↓αgo to*
␈↓ ↓H␈↓αloop]␈↓.

␈↓ ↓H␈↓This expression can be replaced by

␈↓ ↓H␈↓        ␈↓↓a * loop <u, ␈↓¬NIL␈↓↓>␈↓

␈↓ ↓H␈↓and the recursive definition

␈↓ ↓H␈↓        ␈↓↓loop z ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧␈↓αa␈↓↓␈α∧z ␈↓αthen␈↓↓ ␈↓αad␈↓↓␈α∧z ␈↓αelse␈↓↓ loop <␈↓αda␈↓↓␈α∧z, ␈↓αaa␈↓↓␈α∧z . ␈↓αad␈↓↓␈α∧z>␈↓.

␈↓ ↓H␈↓        Should␈α
a␈α
program␈αmake␈α
assignments␈α
to␈α
external␈αvariables,␈α
an␈α
ambiguity␈α
arises.␈α Suppose␈α
we
␈↓ ↓H␈↓evaluate the expression

␈↓ ↓H␈↓        ␈↓↓<x, ␈↓αprogram␈↓↓[[] x ← ␈↓αd␈↓↓␈α∧x], x>␈↓.

␈↓ ↓H␈↓when␈α␈↓↓x␈↓␈αhas␈αthe␈αvalue␈α(A␈αB).␈α If␈αthe␈αarguments␈αof␈αthe␈αlist␈αare␈α"executed"␈αin␈αright␈αto␈αleft␈αorder,␈αthe
␈↓ ↓H␈↓expression␈α
will␈αhave␈α
value␈α
((A␈αB)␈α
(B)␈α(B)),␈α
whereas␈α
if␈αthe␈α
execution␈αis␈α
from␈α
right␈αto␈α
left,␈αthe␈α
value
␈↓ ↓H␈↓will␈αbe␈α
((B)␈α(B)␈α
(A␈αB)).␈α
 However,␈αthe␈αmathematical␈α
semantics␈αof␈α
expressions␈αdon't␈α
prescribe␈αany
␈↓ ↓H␈↓order␈α
of␈αevaluation,␈α
and␈α
experience␈αwith␈α
ALGOL␈α
60,␈αwhich␈α
prescribed␈α
left-to-right␈αevaluation␈α
in
␈↓ ↓H␈↓order␈α
to␈α
give␈α
a␈αdefinite␈α
meaning␈α
to␈α
function␈α
procedures␈αthat␈α
alter␈α
external␈α
variables,␈α
has␈αshown
␈↓ ↓H␈↓that the quality of compiled code is greatly reduced by prescribing a fixed order.

␈↓ ↓H␈↓        This␈α
ambiguity␈αcan␈α
be␈α
resolved␈αby␈α
rewriting␈α
expressions␈αcontaining␈α
programs␈α
that␈αchange
␈↓ ↓H␈↓variables␈α
in␈α
the␈α
expression␈α
using␈α
lambda␈αexpressions␈α
to␈α
force␈α
a␈α
desired␈α
order␈α
of␈αevaluation.␈α
 Thus
␈↓ ↓H␈↓the above expression could be written

␈↓ ↓H␈↓        ␈↓↓[λy:[λz:<z,y,y>][␈↓αprogram␈↓↓[[] x ← ␈↓αd␈↓↓␈α∧x]]][x]␈↓

␈↓ ↓H␈↓which␈α⊂would␈α⊂evaluate␈α⊂to␈α⊂((B)␈α⊂(A␈α⊂B)␈α⊂(A␈α⊂B))␈α⊂in␈α⊂the␈α⊂above␈α⊂case.␈α⊂ Seven␈α⊂other␈α⊂results␈α⊃could␈α⊂be
␈↓ ↓H␈↓obtained␈α
by␈α
putting␈α
different␈α
combinations␈α
of␈α∞␈↓↓z␈↓␈α
and␈α
␈↓↓y␈↓␈α
between␈α
the␈α
pointy␈α
brackets.␈α∞ Once␈α
these
␈↓ ↓H␈↓ambiguities␈α
have␈α
been␈α
resolved,␈α
it␈α
would␈α
seem␈α
that␈α
we␈α
could␈α
translate␈α
an␈α
outer␈α
sequential␈α
program
␈↓ ↓H␈↓containing␈αinner␈αsequential␈αprograms␈αinto␈αa␈αfunction␈αprogram␈αin␈αa␈αunique␈αway␈αeven␈αallowing␈αthe
␈↓ ↓H␈↓inner␈αprograms␈αto␈αmake␈αassignments␈αto␈αvariables␈αin␈αthe␈αouter␈αprograms.␈α The␈αrules␈αfor␈αdoing␈α
this
␈↓ ↓H␈↓haven't been worked out, however.

␈↓ ↓H␈↓        An␈α∪assignment␈α∪may␈α∪be␈α∩regarded␈α∪as␈α∪an␈α∪␈↓αprogram␈↓␈α∩expression.␈α∪ Thus␈α∪␈↓↓[x ← qa y].z␈↓␈α∪is␈α∩an
␈↓ ↓H␈↓abbreviation for ␈↓αprogram␈↓↓[[]x ← y].z␈↓.

␈↓ ↓H␈↓Exercises:
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 95


␈↓ ↓H␈↓        1.␈α
Write␈α
a␈α
LISP␈α
predicate␈α
that␈α
will␈α
determine␈α
whether␈α
a␈α
PROG␈α
in␈α
internal␈α∞form␈α
satisfies
␈↓ ↓H␈↓the above conditions for replacement by a functional term.

␈↓ ↓H␈↓        2.␈α⊃Given␈α⊃that␈α⊃a␈α∩PROG␈α⊃satisfies␈α⊃the␈α⊃conditions,␈α⊃write␈α∩a␈α⊃LISP␈α⊃functions␈α⊃to␈α∩convert␈α⊃the
␈↓ ↓H␈↓PROG expression and give the a list of the required auxiliary function definitions.

␈↓ ↓H␈↓        The␈αreason␈α
for␈αdiscussing␈αhow␈α
to␈αrewrite␈αthe␈α
sequential␈αprogram␈αas␈α
a␈αfunctional␈αprogram␈α
is
␈↓ ↓H␈↓to␈αapply␈αthe␈αthe␈αtheory␈αof␈αchapter␈α3␈α
to␈αthe␈αsequential␈αcase.␈α The␈αabove␈αconditions␈αpermit␈αa␈α
purely
␈↓ ↓H␈↓local␈α∞rewrite,␈α∞but␈α∞it␈α∞seems␈α∞evident␈α∞that␈α∞if␈α∞an␈α∞outer␈α∞sequential␈α∞program␈α∞containing␈α∞an␈α∂inner␈α∞one
␈↓ ↓H␈↓satisfies␈α
the␈α
initialization␈α∞and␈α
local␈α
assignment␈α
(i.e.␈α∞ no␈α
side-effect)␈α
conditions,␈α
then␈α∞the␈α
program
␈↓ ↓H␈↓can␈αbe␈αconverted␈αto␈αfunctional␈αform␈αeven␈αif␈αit␈αcontains␈αsequential␈αsubprograms␈αthat␈αviolate␈αthese
␈↓ ↓H␈↓conditions␈α⊂provided␈α⊃that␈α⊂all␈α⊃assignments␈α⊂in␈α⊂the␈α⊃inner␈α⊂program␈α⊃are␈α⊂at␈α⊂least␈α⊃local␈α⊂to␈α⊃the␈α⊂outer
␈↓ ↓H␈↓program.  The rules for doing this have not been formulated as yet.

␈↓ ↓H␈↓        There␈α⊂are␈α⊂three␈α⊂circumstances␈α⊂in␈α∂which␈α⊂sequential␈α⊂programs␈α⊂are␈α⊂preferred␈α⊂to␈α∂functional
␈↓ ↓H␈↓programs:

␈↓ ↓H␈↓        1.␈αIn␈αsome␈αcases␈αand␈αfor␈αsome␈αpeople,␈αit␈αis␈αeasier␈αto␈αthink␈αabout␈αhow␈αto␈αgo␈αfrom␈αthe␈αinitial
␈↓ ↓H␈↓conditions␈α
step-by-step␈α
to␈α
the␈α
final␈α
result␈α
than␈α
to␈α
think␈α
about␈α
how␈α
the␈α
final␈α
result␈α
can␈αbe␈α
obtained
␈↓ ↓H␈↓from␈α∩easier␈α∩cases.␈α∩ There␈α∩seems␈α∩to␈α∩be␈α∩a␈α∩matter␈α∩of␈α∩taste␈α∩to␈α∩a␈α∩substantial␈α∩extent,␈α∪though␈α∩the
␈↓ ↓H␈↓functional form seems to have clear conceptual advantages for functions like ␈↓↓append␈↓ and ␈↓↓subst␈↓.

␈↓ ↓H␈↓        2.␈αWhen␈αthere␈αare␈αa␈αlarge␈αnumber␈αof␈αvariables,␈αit␈αcan␈αturn␈αout␈αthat␈αthe␈αnecessary␈αfunctions
␈↓ ↓H␈↓have an unwieldy number of arguments.

␈↓ ↓H␈↓        3.␈α⊃When␈α∩we␈α⊃are␈α∩considering␈α⊃a␈α∩program␈α⊃that␈α∩interacts␈α⊃with␈α∩an␈α⊃environment␈α∩instead␈α⊃of
␈↓ ↓H␈↓producing an answer, the sequential form may be required, although this hasn't been proved.

␈↓ ↓H␈↓Remarks:

␈↓ ↓H␈↓        1.␈αBesides␈α(SETQ␈αvar␈αexp),␈αmost␈αLISPs␈αallow␈α(SET␈αexp1␈αexp2),␈αwhere␈α␈↓↓exp1␈↓␈αis␈αevaluated␈αto
␈↓ ↓H␈↓determine␈αto␈αwhat␈αvariable␈αthe␈αassignment␈αis␈αto␈αbe␈αmade.␈α If␈α␈↓↓exp1␈↓␈αdoesn't␈αevaluate␈αto␈αa␈αvariable,
␈↓ ↓H␈↓an error is signalled.

␈↓ ↓H␈↓        2. LISP admits arrays.





␈↓ ↓H␈↓2.  ␈↓αPseudo-functions that modify list structures␈↓


␈↓ ↓H␈↓        In␈α⊃pure␈α∩LISP,␈α⊃list␈α⊃structure␈α∩is␈α⊃never␈α⊃changed.␈α∩ ␈↓↓car␈↓␈α⊃and␈α⊃␈↓↓cdr␈↓␈α∩merely␈α⊃move␈α⊃about␈α∩in␈α⊃list
␈↓ ↓H␈↓structure,␈αand␈α␈↓↓cons␈↓␈αcreates␈αnew␈αlist␈αstructure␈α
from␈αthe␈αfree␈αstorage␈αlist.␈α Of␈αcourse,␈αa␈α
variable␈αcan
␈↓ ↓H␈↓get␈αa␈αnew␈α
value␈αthat␈αcorresponds,␈αfor␈α
instance,␈αto␈αputting␈αan␈α
element␈αon␈αthe␈αend␈α
of␈αa␈αlist,␈α
but␈αin
␈↓ ↓H␈↓pure␈α∞LISP␈α
this␈α∞can␈α
only␈α∞be␈α
accomplished␈α∞by␈α∞creating␈α
new␈α∞list␈α
structure.␈α∞ In␈α
this␈α∞section␈α∞we␈α
will
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 96


␈↓ ↓H␈↓discuss␈αoperations␈αthat␈αactually␈αmodify␈αlist␈αstructure.␈α They␈αoften␈αhave␈αefficiency␈α
advantages,␈αbut
␈↓ ↓H␈↓there␈α
use␈α
interferes␈αwith␈α
saving␈α
memory␈αby␈α
using␈α
merging␈αlist␈α
structure,␈α
and␈αit␈α
is␈α
techniques␈αfor
␈↓ ↓H␈↓proving correctness of such programs are not well developed.

␈↓ ↓H␈↓        The␈α∀simplest␈α∀way␈α∀to␈α∀express␈α∀operations␈α∀that␈α∀modify␈α∀list␈α∀structure␈α∀is␈α∀in␈α∀the␈α∀form␈α∪of
␈↓ ↓H␈↓assignments to ␈↓↓car-cdr␈↓ chains of variables, e.g. we may write

␈↓ ↓H␈↓        ␈↓↓␈↓αada␈↓↓␈α∧x ← y.z␈↓.

␈↓ ↓H␈↓The␈α
effect␈αof␈α
executing␈α
this␈αstatement␈α
is␈αto␈α
replace␈α
the␈α␈↓αada␈↓␈α∧part␈α
of␈αthe␈α
list␈α
structure␈αpointed␈α
to␈αby␈α
␈↓↓x␈↓
␈↓ ↓H␈↓with␈αthe␈αvalue␈αof␈αthe␈α
right␈αhand␈αside.␈α As␈αan␈α
expression,␈αthe␈αstatement␈αtakes␈αthe␈α
value␈αassigned.
␈↓ ↓H␈↓In␈α∞internal␈α∞notation,␈α∂we␈α∞use␈α∞the␈α∂pseudo-functions␈α∞(RPLACA X Y)␈α∞and␈α∂(RPLACD X Y)␈α∞which
␈↓ ↓H␈↓correspond to the statements

␈↓ ↓H␈↓        ␈↓↓␈↓αa␈↓↓␈α∧x ← y␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓↓␈↓αd␈↓↓␈α∧x ← y␈↓

␈↓ ↓H␈↓respectively.

␈↓ ↓H␈↓        RPLACA␈αand␈αRPLACD␈αare␈αhighly␈αunclean.␈α Thus␈αthe␈αeffect␈αof␈αevaluating␈α
an␈αexpression
␈↓ ↓H␈↓involving␈αRPLACA␈αor␈αRPLACD␈αdepends␈αon␈αthe␈αstate␈αof␈αlist␈αstructure␈αand␈αnot␈αmerely␈αon␈αthe␈αS-
␈↓ ↓H␈↓expressions␈α
the␈α
variables␈α
have␈α
as␈α
values.␈α
 Suppose,␈αfor␈α
example,␈α
that␈α
the␈α
variables␈α
␈↓↓x1␈↓␈α
and␈α␈↓↓x2␈↓␈α
each
␈↓ ↓H␈↓have␈αthe␈α
value␈α(A␈αB),␈α
and␈αconsider␈αthe␈α
effect␈αof␈α(SETQ␈α
Z␈α(RPLACA␈α(CDR␈α
X)␈αC)).␈α Z␈α
gets␈αthe
␈↓ ↓H␈↓value␈α
(C),␈α
and␈α
X␈α
gets␈α
the␈α
values␈α
(A␈α
C),␈α
but␈αthe␈α
new␈α
value␈α
of␈α
Y␈α
depends␈α
on␈α
whether␈α
its␈α
copy␈αof␈α
(A
␈↓ ↓H␈↓B)␈α
is␈α
the␈α
same␈α
list␈α
structure␈α
as␈α
X's␈α
copy.␈α
 If␈αyes,␈α
the␈α
new␈α
value␈α
of␈α
Y␈α
is␈α
also␈α
(A␈α
C);␈α
otherwise␈αits
␈↓ ↓H␈↓value remains (A B).

␈↓ ↓H␈↓        The␈α⊂uncleanliness␈α⊃of␈α⊂RPLACA␈α⊂and␈α⊃RPLACD␈α⊂means␈α⊂that␈α⊃the␈α⊂programmer␈α⊃must␈α⊂know
␈↓ ↓H␈↓exactly what list structures merge.  A typical application is the pseudo-function ␈↓↓nconc␈↓ defined by

␈↓ ↓H␈↓        ␈↓↓nconc[u,v] ← ␈↓αprog␈↓↓ram[[w];
␈↓ ↓H␈↓↓        ␈↓αn␈↓↓␈α∧u ← ␈↓αreturn␈↓↓ v;
␈↓ ↓H␈↓↓        w ← u;
␈↓ ↓H␈↓↓loop:   ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧␈↓αd␈↓↓␈α∧w ␈↓αthen␈↓↓ qbegin ␈↓αd␈↓↓␈α∧w ← v; ␈↓αreturn␈↓↓ u qend;
␈↓ ↓H␈↓↓        w ← ␈↓αd␈↓↓␈α∧w;
␈↓ ↓H␈↓↓        ␈↓αgo␈↓↓ loop]␈↓.


␈↓ ↓H␈↓␈↓↓nconc␈↓ can also be given a definition that has the form of a recursive program, namely

␈↓ ↓H␈↓        ␈↓↓nconc[u,v] ← nconc1[u,u,v]␈↓

␈↓ ↓H␈↓with

␈↓ ↓H␈↓        ␈↓↓nconc[u,w,v] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧w ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧␈↓αd␈↓↓␈α∧w ␈↓αthen␈↓↓ [λz:u][rplacd[w,v]] ␈↓αelse␈↓↓ nconc[u, ␈↓αd␈↓↓␈α∧w, v]␈↓.
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 97


␈↓ ↓H␈↓        The␈α⊃value␈α⊃of␈α⊂␈↓↓nconc[u,v]␈↓␈α⊃is␈α⊃just␈α⊂␈↓↓u*v,␈↓␈α⊃but␈α⊃it␈α⊂achieves␈α⊃this␈α⊃result␈α⊂by␈α⊃modifying␈α⊃the␈α⊂last
␈↓ ↓H␈↓element␈αof␈α␈↓↓u␈↓␈αto␈αpoint␈αto␈α␈↓↓v.␈↓␈α It␈αis␈αtypically␈αused␈αwhen␈αno␈αother␈αvariable␈αpoints␈αto␈αlist␈αstructure␈α
that
␈↓ ↓H␈↓merges␈α
into␈α␈↓↓u,␈↓␈α
and␈αthe␈α
old␈α
value␈αof␈α
␈↓↓u␈↓␈αwill␈α
not␈αbe␈α
used␈α
again.␈α In␈α
that␈αcase,␈α
␈↓↓nconc␈↓␈αis␈α
advantageous,
␈↓ ↓H␈↓because␈α
it␈α
does␈αno␈α
␈↓↓cons␈↓es,␈α
and␈α
thus␈αcan't␈α
initiate␈α
garbage␈α
collection.␈α No␈α
formal␈α
methods␈α
exist␈αat
␈↓ ↓H␈↓present for proving that these conditions are met.

␈↓ ↓H␈↓        RPLACD␈α∂can␈α∂also␈α∂be␈α∂used␈α∂to␈α∂insert␈α∂an␈α∂element␈α∂into␈α∂the␈α∂middle␈α∂of␈α∂a␈α∂list.␈α⊂ Suppose,␈α∂for
␈↓ ↓H␈↓example,␈αthat␈αwe␈αwish␈αto␈αinsert␈αthe␈αatom␈αB␈αafter␈αevery␈αoccurrence␈αof␈αthe␈αatom␈αA␈αin␈αa␈αlist␈α␈↓↓u.␈↓␈α We
␈↓ ↓H␈↓can␈αdefine␈αa␈αpure␈α
LISP␈αfunction␈αthat␈αgives␈αa␈α
list␈αobtained␈αfrom␈αthe␈αlist␈α
␈↓↓u␈↓␈αby␈αinserting␈αsuch␈αB's␈α
as
␈↓ ↓H␈↓follows:

␈↓ ↓H␈↓        ␈↓↓insertb u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓␈α∧u = A ␈↓αthen␈↓↓ A.[B.insertb ␈↓αd␈↓↓␈α∧u] ␈↓αelse␈↓↓ ␈↓αa␈↓↓␈α∧u . insertb ␈↓αd␈↓↓␈α∧u␈↓.

␈↓ ↓H␈↓Computing␈α␈↓↓insertb␈αu␈↓␈αdoes␈αnot␈αchange␈αthe␈αvalue␈αof␈α␈↓↓u,␈↓␈αbecause␈αnew␈αlist␈αstructure␈αis␈αmanufactured.
␈↓ ↓H␈↓On the other hand, if we define

␈↓ ↓H␈↓        ␈↓↓insertb2 u ← ␈↓αprog␈↓↓ram[[w];
␈↓ ↓H␈↓↓        w ← u;
␈↓ ↓H␈↓↓loop:   ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧w ␈↓αthen␈↓↓ ␈↓αreturn␈↓↓ u;
␈↓ ↓H␈↓↓        ␈↓αif␈↓↓ ␈↓αa␈↓↓␈α∧w = A ␈↓αthen␈↓↓ ␈↓αd␈↓↓␈α∧w ← B . ␈↓αd␈↓↓␈α∧w;
␈↓ ↓H␈↓↓        w ← ␈↓αd␈↓↓␈α∧w;
␈↓ ↓H␈↓↓        ␈↓αgo␈↓↓ loop]␈↓,


␈↓ ↓H␈↓we␈αget␈α
a␈αprogram␈α
that␈αdoes␈α
the␈αactual␈α
insertions.␈α It␈αis␈α
faster,␈αbecause␈α
it␈αuses␈α
fewer␈α␈↓↓cons␈↓es,␈α
but␈αit
␈↓ ↓H␈↓will␈α⊂damage␈α⊂any␈α⊂list␈α∂structure␈α⊂that␈α⊂merges␈α⊂with␈α⊂that␈α∂representing␈α⊂␈↓↓u,␈↓␈α⊂and␈α⊂it␈α⊂is␈α∂mathematically
␈↓ ↓H␈↓recalcitrant.



␈↓ ↓H␈↓3.  ␈↓αRE-ENTRANT LIST STRUCTURE␈↓


␈↓ ↓H␈↓        So␈α
far␈αwe␈α
have␈α
only␈αconsidered␈α
list␈α
structure␈αin␈α
which␈α
all␈α␈↓↓car-cdr␈↓␈α
chains␈α
terminate␈αin␈α
atoms.
␈↓ ↓H␈↓Mathematically␈αinfinite␈αlist␈αstructures␈αare␈αalso␈αpossible.␈α They␈αcan't␈αbe␈αrepresented␈αin␈αa␈αcomputer,
␈↓ ↓H␈↓but␈αsince␈αthey␈αcan␈αsatisfy␈αthe␈αLISP␈αalgebraic␈αaxioms,␈αwe␈αhave␈αhad␈αto␈αexclude␈αthem␈αin␈αour␈αproofs
␈↓ ↓H␈↓by␈α
axiom␈α
schemata␈α
of␈αinduction.␈α
 Another␈α
possibility␈α
is␈α
the␈αre-entrant␈α
list␈α
structure.␈α
 These␈αcan␈α
be
␈↓ ↓H␈↓created␈αby␈αthe␈αRPLACA␈αand␈αRPLACD␈αoperations.␈α For␈αexample,␈αif␈αthe␈αvariable␈α␈↓↓x␈↓␈αhas␈αvalue␈α(A
␈↓ ↓H␈↓B), executing the statement

␈↓ ↓H␈↓        ␈↓↓␈↓αa␈↓↓␈α∧x ← x␈↓

␈↓ ↓H␈↓gives rise to a circular structure like that of figure 1a.  If we then execute

␈↓ ↓H␈↓        ␈↓↓␈↓αd␈↓↓␈α∧x ← x␈↓

␈↓ ↓H␈↓we␈α∞get␈α∞the␈α
doubly␈α∞re-entrant␈α∞structure␈α∞of␈α
figure␈α∞1b.␈α∞ Other␈α∞possibilities␈α
are␈α∞shown␈α∞in␈α∞the␈α
other
␈↓ ↓H␈↓parts of figure 1.
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 98


␈↓ ↓H␈↓        Re-entrant␈αlist␈αstructures␈αdo␈αnot␈αcorrespond␈α
to␈αS-expressions,␈αand␈αthe␈αcorrectness␈αof␈αmost␈α
of
␈↓ ↓H␈↓programs␈α
given␈α
in␈α
this␈α
book␈α
depends␈α
on␈α
the␈α
data␈α
being␈α
non-re-entrant.␈α
 Re-entrant␈α
structures␈α
can
␈↓ ↓H␈↓be␈α⊂represented␈α⊂by␈α⊃S-expressions␈α⊂provided␈α⊂certain␈α⊃atoms␈α⊂are␈α⊂reserved␈α⊂for␈α⊃use␈α⊂as␈α⊂labels␈α⊃and␈α⊂a
␈↓ ↓H␈↓suitable␈αconvention␈α
is␈αadopted␈αfor␈α
distinguishing␈αordinary␈α
atoms␈αfrom␈αlabels␈α
and␈αpointers␈α
to␈αthe
␈↓ ↓H␈↓labels.␈α∞ For␈α∞example,␈α∞the␈α
structure␈α∞of␈α∞figure␈α∞1b␈α
might␈α∞be␈α∞represented␈α∞by␈α∞((LABEL␈α
A).((POINT
␈↓ ↓H␈↓A).(POINT␈αA))).␈α Programs␈αthat␈αcompute␈αwith␈αre-entrant␈αstructures␈αneed␈αto␈αkeep␈αlists␈αof␈αvertices
␈↓ ↓H␈↓they␈αhave␈αvisited␈αso␈αthat␈αthey␈αcan␈αtell␈αwhen␈αthey␈αare␈αabout␈αto␈αre-enter.␈α Thus␈αthe␈αequivalence␈αof
␈↓ ↓H␈↓merging list structure can be tested by the predicate

␈↓ ↓H␈↓        ␈↓↓equiv[x,y] ← equiv1[x,y,␈↓¬NIL␈↓↓] ≠ LOSE␈↓

␈↓ ↓H␈↓where

␈↓ ↓H␈↓        ␈↓↓equiv1[x,y,u]␈α∩←␈α∩␈↓αif␈↓↓␈α∩x␈α∩␈↓αeq␈↓↓␈α∩y␈α∩∨␈α∩match[x,y,u]␈α∩␈↓αthen␈↓↓␈α∩u␈α∩␈↓αelse␈↓↓␈α∩␈↓αif␈↓↓␈α∩u␈α∩=␈α∩LOSE␈α∩∨␈α∩␈↓αat␈↓↓␈αεx␈α∩∨␈α∩␈↓αat␈↓↓␈αεy␈α⊃∨
␈↓ ↓H␈↓↓unmatch[x,y,u] ␈↓αthen␈↓↓ LOSE ␈↓αelse␈↓↓ equiv1[␈↓αd␈↓↓␈α∧x,␈↓αd␈↓↓␈α∧y,equiv1[␈↓αa␈↓↓␈α∧x,␈↓αa␈↓↓␈α∧y,[x.y].u]]␈↓,

␈↓ ↓H␈↓        ␈↓↓match[x,y,u] ← ¬␈↓αn␈↓↓␈α∧u ∧ [x.y ␈↓αeq␈↓↓ual ␈↓αa␈↓↓␈α∧u ∨ match[x,y,␈↓αd␈↓↓␈α∧u]]␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓↓unmatch[x,y,u] ← ¬␈↓αn␈↓↓␈α∧u ∧ [x = ␈↓αaa␈↓↓␈α∧u ∨ y = ␈↓αda␈↓↓␈α∧u ∨ unmatch[x,y,␈↓αd␈↓↓␈α∧u]]␈↓.

␈↓ ↓H␈↓EXERCISES

␈↓ ↓H␈↓        #. Write a program to list the atoms in a possibly re-entrant list structure.

␈↓ ↓H␈↓        #.␈αWrite␈αa␈αprogram␈α
to␈αtranslate␈αa␈αgraph␈α
description␈αfrom␈αthe␈αnotation␈α
of␈αChapter␈α1␈αto␈αa␈α
re-
␈↓ ↓H␈↓entrant list structure.

␈↓ ↓H␈↓        #.␈α
Write␈αfunctions␈α
to␈αtranslate␈α
in␈α
each␈αdirection␈α
between␈αpossibly␈α
re-entrant␈α
structures␈αand
␈↓ ↓H␈↓the S-expressions corresponding to them using the LABEL, POINTER notation described above.

␈↓ ↓H␈↓        #.␈α
Write␈α
an␈α∞axiom␈α
schema␈α
of␈α∞induction␈α
for␈α
finite␈α∞possibly␈α
re-entrant␈α
list␈α∞structures.␈α
 Hint:
␈↓ ↓H␈↓The␈αschema␈α
can␈αbe␈αbaased␈α
on␈αan␈αassertion␈α
of␈αconvergence␈αof␈α
a␈αprogram␈αthat␈α
scans␈αa␈αlist␈α
structure
␈↓ ↓H␈↓keeping track of the vertices it has alread visited.



␈↓ ↓H␈↓4.  ␈↓αProperty Lists␈↓
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 99


␈↓ ↓H␈↓1. Sequential programs

␈↓ ↓H␈↓2. Side effects

␈↓ ↓H␈↓3. Property lists

␈↓ ↓H␈↓4. Input and output

␈↓ ↓H␈↓5. EXPRS, FEXPRS, LEXPRS, SUBRS, FSUBRS, LEXPRS